/*
 * Copyright 2011 Fabian Wenzelmann
 * 
 * This file is part of Recognition-Procedures-for-Boolean-Functions.
 * 
 * Recognition-Procedures-for-Boolean-Functions is free software: you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation, either version 3 of the License, or
 * (at your option) any later version.
 * 
 * Recognition-Procedures-for-Boolean-Functions is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 * 
 * You should have received a copy of the GNU General Public License
 * along with Recognition-Procedures-for-Boolean-Functions.  If not, see <http://www.gnu.org/licenses/>.
 */

package de.wenzelmf.booleanFunction.dnf;

import java.util.AbstractSet;

/**
 * Class representing DNFs, i.e. a set of Clauses.
 * 
 * Because sets can be implemented in several ways this class is an abstract class. It extends
 * the Java AbstractSet class which is a skeleton implementation of the Set interface.
 * 
 * @author Fabian Wenzelmann
 * @version 1.0
 *
 */
public abstract class DNF extends AbstractSet<Clause>
{
	
	public DNF()
	{
		;
	}

	/**
	 * Returns a String representation of this DNF in set notation (puts all clauses in curly brackets, separated by commas).
	 * The clause set representations are generated by calling {@link Clause#toSetString()}. 
	 * 
	 * @return "{c<sub>1</sub>, c<sub>2</sub>, &hellip;, c<sub>m</sub>}" where c<sub>1</sub>, c<sub>2</sub>, &hellip;, c<sub>m</sub>
	 * are the clauses in this DNF.
	 * @see Clause#toSetString()
	 */
	public String toSetString()
	{
		StringBuilder result = new StringBuilder();
		result.append("{");
		boolean first = true;
		for(Clause c : this)
		{
			if(first)
			{
				first = false;
			}
			else
			{
				result.append(", ");
			}
			result.append(c.toSetString());
		}
		result.append("}");
		return result.toString();
	}
	
	/**
	 * Returns a formula representation of this DNF.
	 * 
	 * @param clauseSeparator The character that is used to separate the clauses.
	 * @param literalSeparator
	 * 
	 * @return "()" if this DNF is empty, "c" if this set is a singleton containing the clause c
	 * and "(c<sub>1</sub> sep c<sub>2</sub> sep &hellip; sep c<sub>m</sub>)" if m &ge; 2 and c<sub>1</sub>, c<sub>2</sub>, &hellip;, c<sub>n</sub>
	 * are the elements in this DNF and sep is the given clauseSeparator character.
	 * 
	 * The clause Strings are generated by calling the method {@link Clause#toFormulaString(char)} on them using literalSeparator.
	 * 
	 * @see Clause#toFormulaString(char)
	 */
	public String toFormulaString(char clauseSeparator, char literalSeparator)
	{
		if(size() == 1)
		{
			for(Clause c : this)
				return c.toFormulaString(literalSeparator);
		}
		StringBuilder result = new StringBuilder();
		result.append("(");
		boolean first = true;
		for(Clause c : this)
		{
			if(first)
			{
				first = false;
			}
			else
			{
				result.append(" ");
				result.append(clauseSeparator);
				result.append(" ");
			}
			result.append(c.toFormulaString(literalSeparator));
		}
		result.append(")");
		return result.toString();
	}
	
	/**
	 * Returns the set String representation of this DNF as returned by {@link #toSetString()}.
	 * 
	 * @see #toSetString()
	 */
	@Override
	public String toString()
	{
		return toSetString();
	}
	
	/**
	 * Returns true if {@code other} is also a DNF and contains the same clauses as this DNF.
	 */
	@Override
	public boolean equals(Object other)
	{
		if(other == this)
			return true;
		if(!(other instanceof DNF))
			return false;
		DNF otherDNF = (DNF)other;
		if(this.size() != otherDNF.size())
			return false;
		// TODO: does it make sense?
		if(this.hashCode() != otherDNF.hashCode())
			return false;
		for(Clause c : this)
		{
			if(!otherDNF.contains(c))
				return false;
		}
		return true;
	}
}
